This is part of a bigger project whose aim is to build general
automated tools to
facilitate the design of proof systems. This paper
investigated the problem of checking the correctness of a proof
transformation. Here, we constructed a tool that checks which
rules permute over another. As such permutations are needed in proving the
correctness of proof search strategies, we hope that proof theorists will
benefit from our tool. 

We are currently working on extending to \sellf\ the results detailed in
\cite{miller.ep}, which allow one to check whether an encoded
proof system admits cut-elimination. With this result, we hope to
implement soon a tool that can perform such check automatically.


